\begin{tabbing}
weakPrecondSendR2\=\{\$a:ut2, \$tg:ut2\}\+
\\[0ex]($T$; $t$; $p$; $l$; ${\it ds}$; $P$; $f$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\oplus$([\=Rpre(source($l$);${\it ds}$;"\$a";$p$;$P$); \+
\\[0ex]
\\[0ex]Rsends(${\it ds}$;locl("\$a");Outcome;$l$;"\$tg" : $T$;[\=$<$"\$tg"\+
\\[0ex], $\lambda$$s$,$v$. [if $P$($s$) then $f$($s$,$v$) else $t$ fi ]
\\[0ex]$>$]);
\\[0ex]
\-\\[0ex]Rsframe($l$;"\$tg";[locl("\$a")])])
\-
\end{tabbing}